타입 보존

타입 보존(type preservation, subject reduction)은 항의 타입이 축약 관계에 대해 보존 되는 타입 체계의 성질을 의미한다. \[ (\Gamma \vdash M : A) \to (M \leadsto N) \to (\Gamma \vdash N : A) \]

타입 체계의 설계에 따라서 이러한 성질이 성립하지 않을 수 있다.

• Coq은 positive coinductive 타입을 사용할 경우 타입이 보존되지 않을 수 있다.
• Lean은 몫 타입과 관련된 축약 규칙에 의해 타입이 보존되지 않을 수 있다.